k:Knd, l:IdLnk. isrcvl(l;k)   

latex

Definitions	ff, t  T, P  Q, x:A. B(x), lnk(k), a = b, , b, A, b, s = t, , x:AB(x), x:A  B(x), P & Q, P  Q, Unit, left + right, isrcvl(l;k), Id, IdLnk, Knd, isrcv(k)
Lemmas	IdLnk wf, Id wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, isrcv wf, bool wf, eq lnk wf, lnk wf, bfalse wf